Nuprl Lemma : sp_refl_cl_cancel
13,42
postcript
pdf
T
:Type,
r
:(
T
T
). irrefl(
T
;
r
)
st_anti_sym(
T
;
r
)
(((
r
)\) <
>{
T
}
r
)
latex
Up
gen
algebra
1
Definitions
t
T
,
P
Q
,
,
x
:
A
.
B
(
x
)
Lemmas
xxirrefl
wf
,
xxst
anti
sym
wf
,
rel
le
sp
refl
cl
,
sp
refl
cl
le
rel
,
refl
cl
wf
,
s
part
wf
,
binrel
le
antisymmetry
origin
T:Type, r:(T
T
). irrefl(T;r) 
st_anti_sym(T;r) (((r
)\) <
>{T} r) T:Type, r:(TT). irrefl(T;r) st_anti_sym(T;r) (((r)\) <>{T} r) 
T Qx:A. B(x)